@i locl(a) occurs once
== e@i.kind(e) = locl(a) & e@i. e'@i. kind(e) = locl(a)  kind(e') = locl(a)  e = e' 

latex

---

clarification:

once-p(es;i;a)
== existse-at(es; i; e.(es-kind(es; e) = locl(a)  Knd))
== & alle-at(es;i;e.alle-at(es;i;e'.es-kind(es; e) = locl(a)  Knd
== & alle-at(es;i;e.alle-at(es;i;e'. es-kind(es; e') = locl(a)  Knd
== & alle-at(es;i;e.alle-at(es;i;e'. e = e'  es-E(es))) 

latex

Definitions	P & Q, e@i.P(e), e@i. P(e), P  Q, Knd, kind(e), locl(a), s = t, E
FDL editor aliases	once-p